(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(push)
(pop)
(push)
(assert (= v1 v1 v0 (bvsge #b101110000 #b101110000) v4 v3 v3 (bvsge #b101110000 #b101110000) (bvsge #b101110000 #b101110000)))
(declare-const v7 Bool)
(assert (xor v7 (distinct (_ bv951 10) (_ bv951 10) (_ bv951 10) (_ bv951 10)) v2))
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const _11-0 (_ BitVec 11))
(assert (= v1 v1 v0 (bvsge #b101110000 #b101110000) v4 v3 v3 (bvsge #b101110000 #b101110000) (bvsge #b101110000 #b101110000)))
(declare-const v16 Bool)
(declare-const v18 Bool)
(assert (= v18 (xor v7 (distinct (_ bv951 10) (_ bv951 10) (_ bv951 10) (_ bv951 10)) v2) v16 v11 (or (xor v7 (distinct (_ bv951 10) (_ bv951 10) (_ bv951 10) (_ bv951 10)) v2) v8 v10 v0 (distinct (= v1 v1 v0 (bvsge #b101110000 #b101110000) v4 v3 v3 (bvsge #b101110000 #b101110000) (bvsge #b101110000 #b101110000)) v3 v9 v7) (=> (= v4 v8 v7 v8 v8 v2 (distinct (_ bv951 10) (_ bv951 10) (_ bv951 10) (_ bv951 10)) v3 (bvsge #b101110000 #b101110000) (xor v7 (distinct (_ bv951 10) (_ bv951 10) (_ bv951 10) (_ bv951 10)) v2) (distinct (_ bv951 10) (_ bv951 10) (_ bv951 10) (_ bv951 10))) (distinct (_ bv951 10) (_ bv951 10) (_ bv951 10) (_ bv951 10))) (= (bvsge #b101110000 #b101110000) v7 v7 (bvsge #b101110000 #b101110000) v0 (xor v7 (distinct (_ bv951 10) (_ bv951 10) (_ bv951 10) (_ bv951 10)) v2) (bvsge #b101110000 #b101110000) v1 v7)) (= _11-0 _11-0 _11-0) v7 (= (bvsge #b101110000 #b101110000) v7 v7 (bvsge #b101110000 #b101110000) v0 (xor v7 (distinct (_ bv951 10) (_ bv951 10) (_ bv951 10) (_ bv951 10)) v2) (bvsge #b101110000 #b101110000) v1 v7) (=> (= v1 v1 v0 (bvsge #b101110000 #b101110000) v4 v3 v3 (bvsge #b101110000 #b101110000) (bvsge #b101110000 #b101110000)) (xor v7 (distinct (_ bv951 10) (_ bv951 10) (_ bv951 10) (_ bv951 10)) v2))))
(check-sat)
